When a circuit design is being designed, automatic or semi-automatic processes, such as determining a clock gating function to be used with respect to a memory element, such as for example a flip-flop or a latch, may be utilized. However, as the circuit design may include a large number of signals that are logically connected to each other by combinational logic, performing various computations may be a hard task.
Traditionally, a use of a Binary Decision Datagram (BDD) may be used to enable automatic simplification of complex binary functions represented by the signals of the circuit design. Another option is to represent the logic and a corresponding desired attribute as a Boolean Satisfaction Problem, and use a SAT solver to determine whether the attribute is satisfied of the logic. In some cases, an All-SAT may be used to determine a set of states in the design that hold the desired attribute. Though these approaches enable processing the circuit design, they do not scale well enough, and given design that has many memory units, input signals and/or complex combinational logic, the sizes of the BDDs may be too large to be retained in the memory of a computerized device and the SAT may not provide an answer within a reasonable time. These problems are an aspect of the state-space explosion problem which refers to the fact that the number of distinct states represented by such a circuit design is too high for a computerized device to process. As each signal multiplies the number of states, it can be understood that the size of the state space is exponential in the number of signals/memory units. Therefore, the state-space explosion problem may be a significant problem with regards to automatic or semi-automatic processing of the circuit design.